package edu.uic.cs.cs582.process.impl;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import java.util.TreeSet;

import org.apache.log4j.Logger;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;

import edu.uic.cs.cs582.data.Component;
import edu.uic.cs.cs582.data.SynsetSet;
import edu.uic.cs.cs582.data.Polarity;
import edu.uic.cs.cs582.data.Synset;
import edu.uic.cs.cs582.data.Word;
import edu.uic.cs.cs582.misc.Config;
import edu.uic.cs.cs582.misc.LogHelper;
import edu.uic.cs.cs582.process.SatProcessor;
import edu.uic.cs.cs582.process.impl.SatIndexParser.ComplexIndex;
import edu.uic.cs.cs582.process.impl.SatIndexParser.Index;
import edu.uic.cs.cs582.process.impl.SatIndexParser.SimpleIndex;

public class SatProcessorImpl implements SatProcessor
{
	private static final Logger LOGGER = LogHelper
			.getLogger(SatProcessorImpl.class);

	private TreeSet<Integer> conflictSynsetIndexes = new TreeSet<Integer>();
	private TreeSet<Integer> conflictWordIndexes = new TreeSet<Integer>();

	private Component component = null;

	public SatProcessorImpl(Component component)
	{
		this.component = component;
	}

	@Override
	public boolean processSat(int[][] cnfArrays) throws TimeoutException
	{
		ISolver solver = SolverFactory.newDefault();
		solver.newVar(Config.MAXVAR);
		solver.setTimeoutMs(Config.TIMEOUT);
		for (int[] clause : cnfArrays)
		{
			try
			{
				solver.addClause(new VecInt(clause));
			}
			catch (ContradictionException e)
			{
				if (LOGGER.isDebugEnabled())
				{
					LOGGER.debug("Catch ContradictionException. ");
				}

				for (int i : clause)
				{
					Index index = SatIndexParser.parseIndex(i, component);
					if (index instanceof SimpleIndex)
					{
						conflictSynsetIndexes.add(((SimpleIndex) index)
								.getSynsetIndex());
					}
					else if (index instanceof ComplexIndex)
					{
						conflictWordIndexes.add(((ComplexIndex) index)
								.getWordIndexInOneComponent());
					}
				}
			}
		}

		// if there's conflict happening when add variables into the solver,
		// return false, and there's no need for further checking
		if (!conflictSynsetIndexes.isEmpty() || !conflictWordIndexes.isEmpty())
		{
			return false;
		}
		/////////////////////

		solver.setSearchListener(new ConflictDetectingListener(
				conflictSynsetIndexes, conflictWordIndexes, component));

		LOGGER.debug("Begin to solve SAT. ");
		boolean result = solver.isSatisfiable();
		LOGGER.debug("End to solve SAT. Result is [" + result + "]. ");

		return result;
	}

	@Override
	public Map<Synset, List<Word>> getConflictWordsBySynset()
	{
		Map<Synset, List<Word>> result = new HashMap<Synset, List<Word>>();

		Set<Word> allWords = component.getAllWords();
		List<Synset> allConflictSynsets = getConflictSynset();

		for (Word word : allWords)
		{
			for (Synset conflictingSynset : allConflictSynsets)
			{
				if (isWordHasConflictingMajoritySynset(word, conflictingSynset)
						&& !isWordContainsNonConflictMajoritySynset(word,
								allConflictSynsets))
				{
					List<Word> wordList = result.get(conflictingSynset);
					if (wordList == null)
					{
						wordList = new ArrayList<Word>();
						result.put(conflictingSynset, wordList);
					}
					wordList.add(word);
				}
			}

		}

		return result;
	}

	private List<Synset> getConflictSynset()
	{
		List<Synset> result = new ArrayList<Synset>(
				conflictSynsetIndexes.size());
		for (Integer index : conflictSynsetIndexes)
		{
			result.add(component.getSynsetByIndex(index));
		}

		return result;
	}

	private boolean isWordContainsNonConflictMajoritySynset(Word word,
			List<Synset> allConflictSynsets)
	{
		for (Set<Synset> eachMajority : word.getMajoritySynsets())
		{
			boolean isMajorityContainsConflict = false;
			for (Synset eachConflictSynset : allConflictSynsets)
			{
				if (eachMajority.contains(eachConflictSynset))
				{
					isMajorityContainsConflict = true;
					break;
				}
			}

			if (!isMajorityContainsConflict)
			{
				return true;
			}
		}

		return false;
	}

	private boolean isWordHasConflictingMajoritySynset(Word word,
			Synset conflictingSynset)
	{
		for (Set<Synset> eachMajoritySynsets : word.getMajoritySynsets())
		{
			if (eachMajoritySynsets.contains(conflictingSynset))
			{
				return true;
			}
		}

		return false;
	}

	// FIXME modify the error!!!!
	@Override
	public Map<MajoritySynsets, Set<Word>> getConflictWordsByMajoritySynsets()
	{
		Map<MajoritySynsets, Set<Word>> conflictingWordsByMajoritySynsets = new HashMap<MajoritySynsets, Set<Word>>();

		// for each conflicting word
		for (Integer wordIndex : conflictWordIndexes)
		{
			Word conflictingWord = component.getWordByIndex(wordIndex);
			List<MajoritySynsets> allMajoritySynsetsOfOneWord = conflictingWord
					.getMajoritySynsets();
			// all its majority-synsets are in conflicting
			for (MajoritySynsets majoritySynsets : allMajoritySynsetsOfOneWord)
			{
				Set<Word> conflictingWords = conflictingWordsByMajoritySynsets
						.get(majoritySynsets);
				if (conflictingWords == null)
				{
					conflictingWords = new TreeSet<Word>();
					conflictingWordsByMajoritySynsets.put(majoritySynsets,
							conflictingWords);
				}
				conflictingWords.add(conflictingWord);
			}
		}

		boolean hasChanged = false;
		do
		{
			hasChanged = false;

			for (Word otherWord : component.getAllWords())
			{
				if (conflictWordIndexes.contains(component
						.getIndexOfWord(otherWord)))
				{
					// the conflicting words that have already processed in above steps
					continue;
				}

				// the words that haven't been reported, but may be the cause of conflict

				// if word doesn't have free majority-synsets
				// the word must be inconsistent
				if (!hasConflictFreeMajoritySynsets(otherWord,
						conflictingWordsByMajoritySynsets.keySet()))
				{
					conflictWordIndexes
							.add(component.getIndexOfWord(otherWord));

					for (MajoritySynsets majoritySynsetsOfOtherWord : otherWord
							.getMajoritySynsets())
					{
						Set<Word> conflictingWords = conflictingWordsByMajoritySynsets
								.get(majoritySynsetsOfOtherWord);
						if (conflictingWords == null)
						{
							conflictingWords = new TreeSet<Word>();
							conflictingWordsByMajoritySynsets.put(
									majoritySynsetsOfOtherWord,
									conflictingWords);
							hasChanged = true;
						}

						conflictingWords.add(otherWord);
					}
				}
			}
		}
		while (hasChanged);

		// FIXME need refactor!
		// drop those words been reported as inconsistent but all with same polarity
		HashSet<MajoritySynsets> toDelete = new HashSet<MajoritySynsets>();
		for (Entry<MajoritySynsets, Set<Word>> entry : conflictingWordsByMajoritySynsets
				.entrySet())
		{
			boolean hasDifferentPolarity = false;
			Polarity polarity = null;
			for (Word word : entry.getValue())
			{
				if (polarity == null)
				{
					polarity = word.getPolarity();
				}
				else
				{
					if (polarity != word.getPolarity())
					{
						hasDifferentPolarity = true;
						break;
					}
				}
			}

			if (!hasDifferentPolarity)
			{
				toDelete.add(entry.getKey());
			}
		}
		for (MajoritySynsets majoritySynsetsToDelete : toDelete)
		{
			conflictingWordsByMajoritySynsets.remove(majoritySynsetsToDelete);
		}

		return conflictingWordsByMajoritySynsets;
	}

	private boolean hasConflictFreeMajoritySynsets(Word word,
			Set<MajoritySynsets> allKnownConflictingMajoritySynsets)
	{
		for (MajoritySynsets majoritySynsetsOfWord : word.getMajoritySynsets())
		{
			boolean hasCommon = false;
			for (MajoritySynsets knownConflictingMajoritySynsets : allKnownConflictingMajoritySynsets)
			{
				// the polarities should not be the same one
				// has no common -> there is free
				if (word.getPolarity() != knownConflictingMajoritySynsets
						.getSupposedPolarity()
						&& majoritySynsetsOfWord
								.hasCommon(knownConflictingMajoritySynsets))
				{
					hasCommon = true;
					break;
				}
			}

			if (!hasCommon)
			{
				return true;
			}
		}

		return false;
	}
}
